package kodkod.analysis;

import java.util.*;

import kodkod.analysis.ast.GraphVisitor;
import kodkod.ast.*;
import kodkod.ast.operator.*;

public class FormulaAnalyzer {
	
	Formula formula;
	boolean negated;
	
	ArrayList<FormulaAnalyzer> children = new ArrayList<FormulaAnalyzer>();
	enum Op {
		NONE, TRUE, FALSE, AND, OR, IMPLIES, IFF, NOT, EQUIV, SUBSET, INT, MULT, QUANT, RP
	}
	Op type = Op.NONE;
	
	public FormulaAnalyzer(Formula formula) {
		this(formula, false);
	}
	
	public FormulaAnalyzer(Formula formula, boolean negated) {
		this.formula = formula;
		this.negated = negated;
		
		if (formula instanceof BinaryFormula) {
			BinaryFormula f = (BinaryFormula)formula;
			if (f.op().equals(FormulaOperator.AND)) {
				type = Op.AND;
				children.add(new FormulaAnalyzer(f.left(), negated));
				children.add(new FormulaAnalyzer(f.right(), negated));
			} else if (f.op().equals(FormulaOperator.OR)) {
				type = Op.OR;
				children.add(new FormulaAnalyzer(f.left(), negated));
				children.add(new FormulaAnalyzer(f.right(), negated));
			} else if (f.op().equals(FormulaOperator.IMPLIES)) {
				type = Op.IMPLIES;
				children.add(new FormulaAnalyzer(f.left(), !negated));
				children.add(new FormulaAnalyzer(f.right(), negated));
			} else if (f.op().equals(FormulaOperator.IFF)) {
				type = Op.IFF;
				children.add(new FormulaAnalyzer(f.left(), negated));
				children.add(new FormulaAnalyzer(f.right(), negated));
				children.add(new FormulaAnalyzer(f.left(), !negated));
				children.add(new FormulaAnalyzer(f.right(), !negated));
			}
		} else if (formula instanceof NaryFormula) {
			NaryFormula f = (NaryFormula)formula;
			if (f.op().equals(FormulaOperator.AND)) {
				type = Op.AND;
			} else if (f.op().equals(FormulaOperator.OR)) {
				type = Op.OR;
			}
			for (Formula child : f) {
				children.add(new FormulaAnalyzer(child, negated));
			}
		} else if (formula instanceof NotFormula) {
			NotFormula f = (NotFormula)formula;
			type = Op.NOT;
			children.add(new FormulaAnalyzer(f.formula(), !negated));
		} else if (formula instanceof ComparisonFormula) {
			ComparisonFormula f = (ComparisonFormula)formula;
			if (f.op().equals(ExprCompOperator.EQUALS)) {
				type = Op.EQUIV;
			} else {
				type = Op.SUBSET;
			}
		} else if (formula instanceof ConstantFormula) {
			ConstantFormula f = (ConstantFormula)formula;
			type = f.booleanValue() ? Op.TRUE : Op.FALSE;
		} else if (formula instanceof IntComparisonFormula) {
			IntComparisonFormula f = (IntComparisonFormula)formula;
			type = Op.INT;
		} else if (formula instanceof MultiplicityFormula) {
			MultiplicityFormula f = (MultiplicityFormula)formula;
			type = Op.MULT;
		} else if (formula instanceof QuantifiedFormula) {
			QuantifiedFormula f = (QuantifiedFormula)formula;
			type = Op.QUANT;
			children.add(new FormulaAnalyzer(f.formula(), negated));
		} else if (formula instanceof RelationPredicate) {
			RelationPredicate f = (RelationPredicate)formula;
			type = Op.RP;
		}
	}
	
	class HighlyConstrainingFormulas extends HashMap<Formula, Double> {
		private static final long serialVersionUID = 575964028537493050L;
		
		final double PENALTY = 0.75;
		double penalty = 1.0;
		
		public HighlyConstrainingFormulas() { 
			super();
		}
		
		public HighlyConstrainingFormulas or(HighlyConstrainingFormulas other) {
			for (Formula f : this.keySet()) {
				this.put(f, this.get(f) * other.penalty * PENALTY);
			}
			for (Formula f : other.keySet()) {
				this.put(f, other.get(f) * this.penalty * PENALTY);
			}
			this.penalty *= PENALTY;
			return this;
		}
		
		public HighlyConstrainingFormulas and(HighlyConstrainingFormulas other) {
			this.putAll(other);
			this.penalty = 1.0;
			return this;
		}
	}
	
	public HighlyConstrainingFormulas getHighlyConstrainingFormulas() {
		HighlyConstrainingFormulas hcf = new HighlyConstrainingFormulas();
				
		switch (this.type) {
		case AND:
			for (FormulaAnalyzer child : children) {
				if (!negated) hcf = hcf.and(child.getHighlyConstrainingFormulas());
				else hcf = hcf.or(child.getHighlyConstrainingFormulas());
			}
			break;
		case OR:
		case IMPLIES:
			for (FormulaAnalyzer child : children) {
				if (!negated) hcf = hcf.or(child.getHighlyConstrainingFormulas());
				else hcf = hcf.and(child.getHighlyConstrainingFormulas());
			}
			break;
		case IFF:{
			HighlyConstrainingFormulas child0 = children.get(0).getHighlyConstrainingFormulas();
			HighlyConstrainingFormulas child1 = children.get(1).getHighlyConstrainingFormulas();
			// include negated variant
			HighlyConstrainingFormulas child2 = children.get(2).getHighlyConstrainingFormulas();
			HighlyConstrainingFormulas child3 = children.get(3).getHighlyConstrainingFormulas();
			hcf = child0.and(child1).or(child2.and(child3));
			break;}
		case NOT:
			hcf = children.get(0).getHighlyConstrainingFormulas();
			break;
		case EQUIV:
			// skip self-equalities
			ComparisonFormula compFormula = (ComparisonFormula)formula;
			if (compFormula.left() == compFormula.right()) break;
			if (compFormula.left() instanceof Variable && compFormula.right() instanceof Variable) {
				Expression left = Analyzer.initialAnalysis.decls.get(compFormula.left());
				Expression right = Analyzer.initialAnalysis.decls.get(compFormula.right());
				if (left != null && left == right) break;
			}
			//fall-through:
		case SUBSET:
			if (!negated) hcf.put(formula, 1.0);
			break;
		case INT:
			IntComparisonFormula intComp = (IntComparisonFormula)formula;
			if (!(negated && intComp.op().equals(IntCompOperator.EQ))) {
				Casts pLeft = new Casts(intComp.left());
				Casts pRight = new Casts(intComp.right());
				
				if (pRight.size() == 0 || pLeft.size() == 0) {//constant bound
					hcf.put(formula, 1.0);
				}
			}
			break;
		case MULT:
			MultiplicityFormula multFormula = (MultiplicityFormula)formula;
			if (negated == multFormula.multiplicity().equals(Multiplicity.SOME)) {				
				hcf.put(formula, 1.0);
			}
			break;
		case QUANT:
			QuantifiedFormula qFormula = (QuantifiedFormula)formula;
			if (negated != qFormula.quantifier().equals(Quantifier.ALL)) {
				hcf = children.get(0).getHighlyConstrainingFormulas();
			} else {
				hcf.put(formula, 1.0);
			}
			break;
		case RP:
		case TRUE:
		case FALSE:
		case NONE:
		default:
			hcf = new HighlyConstrainingFormulas();
			break;
		}		
		return hcf;
	}
	
	public double getSolutionRate() {
		double solutionRate = 1.0;
				
		switch (this.type) {
		case TRUE:
			solutionRate = 1.0;
			break;
		case FALSE:
			solutionRate = 0.0;
			break;
		case AND:
			solutionRate = 1.0;
			for (FormulaAnalyzer child : children) {
				solutionRate *= child.getSolutionRate();
			}
			break;
		case OR:
			solutionRate = 0.0;
			for (FormulaAnalyzer child : children) {
				solutionRate = 1 - ((1 - solutionRate) * (1 - child.getSolutionRate()));
			}
			break;
		case IMPLIES:{
			double child0 = children.get(0).getSolutionRate();
			double child1 = children.get(1).getSolutionRate();
			solutionRate = 1 - (child0 * (1 - child1));
			break;}
		case IFF:{
			double child0 = children.get(0).getSolutionRate();
			double child1 = children.get(1).getSolutionRate();
			// include negated variant
			double child2 = children.get(0).getSolutionRate();
			double child3 = children.get(1).getSolutionRate();
			solutionRate = 1 - ((1 - child0 * child1) * (1 - child2 * child3));
			break;}
		case NOT:
			solutionRate = 1 - children.get(0).getSolutionRate();
			break;
		case EQUIV:
			solutionRate = 0.5;
			break;
		case SUBSET:
			solutionRate = 0.75;
			break;
		case INT:
			solutionRate = 0.1;
			break;
		case MULT:
			solutionRate = 0.1;
			break;
		case QUANT:
			solutionRate = children.get(0).getSolutionRate();
			break;
		case RP:
			solutionRate = 1.0;
			break;
		case NONE:
		default:
			solutionRate = 1.0;
			break;
		}	
		
		return solutionRate;
	}
	
	public ArrayList<Expression> getCardinalityBoundedExpressions() {
		ArrayList<Expression> boundedExpressions = new ArrayList<Expression>();
		
		if (formula instanceof IntComparisonFormula) {
			IntComparisonFormula intComp = (IntComparisonFormula)formula;
			IntCompOperator op = intComp.op();
			
			if (!(negated && op.equals(IntCompOperator.EQ))) {
				boolean leftBoundLow = negated == (op.equals(IntCompOperator.GT) || op.equals(IntCompOperator.GTE));
				boolean rightBoundLow = negated == (op.equals(IntCompOperator.LT) || op.equals(IntCompOperator.LTE));
									
				Casts pLeft = new Casts(intComp.left());
				Casts pRight = new Casts(intComp.right());
				
				if (pRight.size() == 0 || pLeft.size() == 0) {//constant bound
					if (leftBoundLow) for (Expression cast : pLeft) boundedExpressions.add(cast);
					if (rightBoundLow) for (Expression cast : pRight) boundedExpressions.add(cast);
				}
			}
		}
		else if (formula instanceof MultiplicityFormula) {
			MultiplicityFormula multFormula = (MultiplicityFormula)formula;
			if (negated == multFormula.multiplicity().equals(Multiplicity.SOME)) {
				boundedExpressions.add(multFormula.expression());
			}
		}
		else {
			for (FormulaAnalyzer child : children) {
				boundedExpressions.addAll(child.getCardinalityBoundedExpressions());
			}
		}
		
		return boundedExpressions;
	}
}
